\section{Стековая машина}

$X$ --- счетное множество переменных, $L$ --- счетное множество меток.
Синтаксис инструкций:

$$
  \begin{array}{rcl}
    \fancy{I}=&\term{E}&\cup\\
      &\term{R}&\cup\\
      &\term{W}&\cup\\
      &\term{C}\NN &\cup\\
      &\term{L}X&\cup\\
      &\term{S}X&\cup\\
      &\term{B}\otimes&\cup\\
      &\term{J}L&\cup\\
      &\term{JT}L&\cup\\
      &\term{JF}L&
  \end{array}
$$

Синтаксис программ: 

$$
  \fancy{P}=\epsilon\cup \{L\fancy{I}\}\fancy{P}
$$

Считается, что все инструкции помечены разными метками.
Семантика стековой машины: множество конфигураций

$$
C=\ZZ^*\times(X\to\ZZ)\times\ZZ^*\times\ZZ^*
$$

Окружение: 

$$
M=L\to\fancy{P}
$$

$$
\withenv{M}{\trans{c}{\inmath{\{l\term{E}\}P}}{c}}\ruleno{E$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{s,m,xi,o}}{\inmath{\{l\term{R}\}P}}{c^\prime}}}\ruleno{R$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{s,i,m,ox}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{\{l\term{W}\}P}}{c^\prime}}}\ruleno{W$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{zs,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{\{l\term{C}z\}P}}{c^\prime}}}\ruleno{C$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{(m\;x)s,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{\{l\term{L}x\}P}}{c^\prime}}}\ruleno{L$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{s,m[x\gets y],i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{ys,m,x,o}}{\inmath{\{l\term{S}x\}P}}{c^\prime}}}\ruleno{S$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{\inbr{(y\oplus x)s,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xys,m,i,o}}{\inmath{\{l\term{B}\otimes\}P}}{c^\prime}}}\ruleno{B$_{sm}$}
$$

$$
\trule{\withenv{M}{\trans{c}{\inmath{M\;n}}{c^\prime}}}
      {\withenv{M}{\trans{c}{\inmath{\{l\term{J}n\}P}}{c^\prime}}}\ruleno{J$_{sm}$}
$$


$$
\crule{\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{M\;n}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{\{l\term{JT}n\}P}}{c^\prime}}}
      {x\ne 0}\ruleno{JT-True$_{sm}$}
$$

$$
\crule{\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{\{l\term{JT}n\}P}}{c^\prime}}}
      {x=0}\ruleno{JT-False$_{sm}$}
$$

$$
\crule{\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{M\;n}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{\{l\term{JF}n\}P}}{c^\prime}}}
      {x=0}\ruleno{JF-True$_{sm}$}
$$

$$
\crule{\withenv{M}{\trans{\inbr{s,m,i,o}}{\inmath{P}}{c^\prime}}}
      {\withenv{M}{\trans{\inbr{xs,m,i,o}}{\inmath{\{l\term{JF}n\}P}}{c^\prime}}}
      {x\ne 0}\ruleno{JF-False$_{sm}$}
$$

Семантика программы: $\sembr{P}_P=\lambda i.o$, где 

$$\withenv{M}{\trans{\inbr{\epsilon,\perp,i,\epsilon}}{\llang{$P$}}{\inbr{s,\epsilon,o}}}$$
$$M=\lambda l.P[l]$$

Свойства стековой машины:

\begin{itemize}
\item сохранение стека;
\item инвариантность относительно ``хвоста''.
\end{itemize}





